(declare-const r1 Real)
(declare-const r7 Real)
(declare-const r8 Real)
(push)
(declare-const r9 Real)
(declare-const v24 Bool)
(declare-const r10 Real)
(declare-const r12 Real)
(assert (or (<= r7 6805.0 (* (/ 7434.32 (/ (- r1 r1 r1 r1) (- r1))) r1 (- r1) (- r1)) (- (- r1))) false))
(assert (or (xor (< 7434.32 7434.32 r1) (= (/ (- r1) r10) (- (/ (- r1 r1 r1 r1) (- r1 r1 r1 r1)) (- r1) 7434.32 60773.0) r8 (- r1) 508987.0) v24) (> (/ (- r1 r1 r1 r1) (- r1 r1 r1 r1)) r10 7434.32 r12 r9) false))
(check-sat)
